`timescale 1ns/1ps
//                                bind           DUT   
module counter_props (
    input logic       clk,
    input logic       rst_n,
    input logic       en,
    input logic [3:0] cnt,
    input logic       ovf
);

//                
default clocking @(posedge clk); endclocking

// ------------------------------
//             
// ------------------------------

//                      0            
property p_reset;
    !rst_n |=> cnt == 0 && ovf == 0;
endproperty
a_reset: assert property (p_reset);

//                                        15   
property p_increment;
    en && cnt < 4'hF |=> cnt == $past(cnt) + 1;
endproperty
a_increment: assert property (p_increment);

//             
property p_overflow;
    en && cnt == 4'hF |=> cnt == 0 && ovf;
endproperty
a_overflow: assert property (p_overflow);

// ------------------------------
//          
// ------------------------------
covergroup cg_counter @(posedge clk);
    coverpoint cnt {
        bins all_values[] = {[0:15]};
    }
    overflow: coverpoint ovf;
endgroup
cg_counter cg = new();

endmodule

//                                counter       
bind counter counter_props props (
    .clk   (clk),
    .rst_n (rst_n),
    .en    (en),
    .cnt   (cnt),
    .ovf   (ovf)
);